Modern design of very large-scale integrated circuits and of complex software systems often involves years of research and the efforts of hundreds of engineers. Automated formal verification methods may be an essential part of the design effort, reducing errors, lost time and risk to financial investment. Formal verification involves building a finite model of a system as a group of states and state transitions and checking that a desired property holds in the model. An exhaustive search of all possible states of the model may be performed in order to verify a desired property.
As the size and complexity of designs increase, much effort may be expended to improve the efficiency of automated formal verification methods. One technique used in symbolic model checking to improve efficiency is to employ binary decision diagrams (BDDs). A BDD is a directed acyclic graph that represents a Boolean expression. FIG. 1, to which reference may be now briefly made, shows an exemplary BDD for the expression ((a1 iff a2) and (b1 iff b2), where “iff” stands for “if and only if”. Each circle indicates a variable (a1, a2, b1, b2) and the lines indicate the directions to follow when the variable has a value of 0 (dashed lines) or 1 (solid lines). For each BDD, there may be two terminal nodes 8 representing the result of the Boolean expression.
Boolean operations performed on a BDD are a polynomial function of the size of the BDD. While BDDs are generally a compact representation of a Boolean expression, they can be exponential in the size of the expression they are representing. In addition, the size of the BDD is significantly affected by the order in which the variables of the expression are listed.
One method for symbolic model checking using BDDs comes from Carnegie Mellon University and is known as the Symbolic Model Verifier (SMV). A good discussion of symbolic model checking may be found in the introduction to the online paper “NuSMV: a new symbolic model checker” by A. Cimatti et al., which can be found in 2003 at the website: nusmv.irst.itc.it/NuSMV/papers/sttt_j/html/paper.html. Another model checker may be Rulebase, commercially available from International Business Machines Inc. (IBM) of the USA, which includes in it a symbolic model checker.
The article by C. Eisner, “Using Symbolic CTL Model Checking to Verify the Railway Stations of Hoorn-Kersenboogerd and Heerhugowaard”, Software Tools for Technology Transfer, Vol. 4, number 1 pp. 107-124, includes a nice tutorial on the process of symbolic model checking.
One of the important functions of symbolic model checkers is to determine which group RS of states of a model may be reached from an initial group S0 of states and which cannot be reached. This is known as “reachability”. FIG. 2, to which reference is now briefly made, is an illustration of a state machine 12 with six states, A, B, C, D, E and F. Each state represents one particular set of assignments of three state variables (v1, v2, v3) forming a state vector ν. Thus, for example, state A is the state with the values (0,0,0) while state C is the state with the values (1,0,1).
State machine 12 moves through the states as indicated by the arrows on FIG. 2. Thus, state machine 12 may remain at state A or it may proceed to state C and from there to state E or it may begin at state B and move to state D. This movement through the groups of state is defined, in symbolic model checking, by a “transition relation” R from one state vector ν to a “next” state vector ν′. For state machine 12, transition relation R is:
      R    ⁡          (                        v          _                ,                              v            _                    ′                    )        =      {                                        (                          000              ⁢                              ,                            ⁢              000                        )                                                            (                          000              ⁢                              ,                            ⁢              101                        )                                                            (                          011              ⁢                              ,                            ⁢              001                        )                                                            (                          101              ⁢                              ,                            ⁢              111                        )                                                            (                          110              ⁢                              ,                            ⁢              011                        )                                }  
From the initial group S0 of states {A, B}, the state machine may get to the group S1 of states {A,C,D} in one step. State A has already been explored and thus, the next step is to explore states C and D. From the group {C,D}, the state machine can get to the group S2 comprised of state E. Since state E has no outward going arrow, the model checker is finished. From these results, the reachable states are A,B,C and D. State F is not reachable from any of the initial states.
A model checker may operate on the graph of FIG. 1 and may follow the arrows, looking for states. A symbolic model checker may perform its checking through use of a symbolic representation of the graph, rather than the graph itself.
The model described above is a Kripke structure M defined over a set of atomic propositions AP. Mathematically, this is written:M=(S,S0,R,L)
where L is a labeling function that labels each state S with the set of atomic propositions that are true in that state S. The states of the Kzipke structure are coded by the group of state variables ν.
The basic operations in symbolic model checking may be the image computation and the pre-image computation. The image computation of Si uses transition relation R to move to the next group of states Si+1. The pre-image computation of Si uses transition relation R to take a step backwards to the group of states Si−1.
More precisely:image(S( ν),R( ν, ν′))=∃ ν(S( ν)R( ν, ν′))andpre_image (S( ν′),R( ν, ν′))=∃ν′(S(ν′)R( ν, ν′))
where S( ν) and R( ν, ν′) are BDDs representing a group of states S and a transition relation R, respectively, ∃ is the ‘exist’ function and  is the ‘and’ function. Computing ∃xA( ν) may be referred to as “quantifying x out of A”. Early existential quantification may make image and pre-image computations more efficient by reducing the size of the BDD.
A “conjunctive partitioned transition relation” may be composed of a set of partitions and_Ri such that, when they are ‘anded’ together, they produce the transition relation R( ν, ν′), or, mathematically:R( ν, ν′)=iand—Ri( ν, ν′i)
If each state variable νi can be described by a single conjunctive partition, then and_Ri=(ν′i=ƒνi( ν)) and thus, each partition may be a function of the current set of variables ν and ν′i (the ith next step variable) rather than the current and next step sets of variables, ν and ν′, respectively. The image computation in this case is:
      image    ⁡          (              S        ⁡                  (                      v            _                    )                    )        =      ∃                  v        _            ⁡              (                  S          ⁢                                    (                              v                _                            )                        ⋀                          (                                                ⋀                                      v                    i                                                  ⁢                                                      and_R                                          v                      i                                                        ⁢                                      (                                                                  v                        _                                            ,                                              v                        i                        ′                                                              )                                                              )                                      )            
A “disjunctive partitioned transition relation” may be composed of a set of partitions or_Ri such that, when they are “or'ed” together, they produce the transition relation R( ν, ν′), or, mathematically:R( ν, ν′)=ior—Ri( ν, ν′)
If each current state variable νi can be changed only in a single disjunctive partition, then
      or_R          v      i        =            (                        v          i          ′                =                              f                          v              i                                ⁡                      (                          v              _                        )                              )        ⋀                  (                              ∀                          y              ≠                                                v                  i                                :                y                                              =                      y            ′                          )            .      The image computation in this case is:
      image    ⁡          (              S        ⁡                  (                      v            _                    )                    )        =      ∃                  v        _            ⁡              (                              S            ⁡                          (                              v                _                            )                                ⋀                      (                                          ⋁                                  v                  i                                            ⁢                                                or_R                                      v                    i                                                  ⁢                                  (                                                            v                      _                                        ,                                                                  v                        _                                            i                      ′                                                        )                                                      )                          )            
Because existential quantification distributes, mathematically, over disjunction, every quantification may be performed before performing the disjunction operation and thus:
      image    ⁡          (              S        ⁡                  (                      v            _                    )                    )        =            ⋁              v        i              ⁢          ∃                        v          _                ⁡                  (                                                    S                ⁡                                  (                                      v                    _                                    )                                            ⋀                              or_R                                  v                  i                                                      ⁢                          (                                                v                  _                                ,                                  v                  i                  ′                                            )                                )                    
Because quantification may be done before disjunction for every variable vi in the disjunctive partitioning, all intermediate BDD results depend only on the set of next step variables ν′, while when using conjunctive partitions, the intermediate BDD results may depend both on the current and next step sets of variables, ν and ν′. Thus, using disjunctive partitions usually results in smaller intermediate BDDs than when using conjunctive partitions.
The following articles discussed the application of symbolic model checking to general purpose software by translating C source code to EDL (Environment Description Language), which may be the input language to the RuleBase model checker:                C. Eisner, “Model checking the garbage collection mechanism of SMV”, In S. D. Stoller and W. Visser, editors, Electronic Notes in Theoretical Computer Science, volume 55, Elsevier Science Publishers, 2001; and        C. Eisner and D. Peled, “Comparing symbolic and explicit model checking of a software system,” In Proceedings, 9th International SPIN Workshop on Model Checking of Software, LNCS 2318, Springer-Verlag, 2002, pages 230-239.        
It will be appreciated that for simplicity and clarity of illustration, elements shown in the figures have not necessarily been drawn to scale. For example, the dimensions of some of the elements may be exaggerated relative to other elements for clarity. Further, where considered appropriate, reference numerals may be repeated among the figures to indicate corresponding or analogous elements.